the_es:ES, e':E, n:.
(n < ||before(e')||)  (firstn(n;before(e')) = before(before(e')[n])  (E List)) 

latex

Definitions

x:A. B(x), P  Q, ||as||, before(e), t  T, , x. t(x), A  B, A, False, Y, if b then t else f fi , tt, i  j , t  ...$L, ff, P  Q, P  Q, P & Q, l[i], SQType(T), {T}, hd(l), nth_tl(n;as), i z j, b, i <z j, Top, S  T, {i..j}, i  j < k, , WellFnd{i}(A;x,y.R(x;y)), x(s), , Unit, Dec(P), P  Q,

Lemmas

es-locl-wellfnd, nat wf, length wf1, es-E wf, es-before wf, firstn wf, select wf, es-first wf, bool wf, eqtt to assert, length nil, length wf2, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, es-pred wf, es-pred-locl, es-locl wf, event system wf, decidable int equal, append wf, select append back, length cons, non neg length, length append, first0, top wf, es-before wf2, Id wf, es-loc wf, firstn append, le wf, firstn length, select append front